right\_child($t$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case($t$) Case $x$;$y$ =$>$ $y$ Default =$>$ $t$